package base;

import utils.FormuleType;
import utils.TransporteurQuantifieurs;
import utils.Skolemisateur;
/**
 *  Copyright (c) 1999-2011, Ecole des Mines de Nantes
 *  All rights reserved.
 *  Redistribution and use in source and binary forms, with or without
 *  modification, are permitted provided that the following conditions are met:
 *
 *      * Redistributions of source code must retain the above copyright
 *        notice, this list of conditions and the following disclaimer.
 *      * Redistributions in binary form must reproduce the above copyright
 *        notice, this list of conditions and the following disclaimer in the
 *        documentation and/or other materials provided with the distribution.
 *      * Neither the name of the Ecole des Mines de Nantes nor the
 *        names of its contributors may be used to endorse or promote products
 *        derived from this software without specific prior written permission.
 *
 *  THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND ANY
 *  EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 *  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 *  DISCLAIMED. IN NO EVENT SHALL THE REGENTS AND CONTRIBUTORS BE LIABLE FOR ANY
 *  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 *  (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 *  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 *  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 *  (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 *  SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */

/**
 * Created by IntelliJ IDEA.
 * User: njussien
 * Date: 30/11/12
 * Time: 10:26
 */
public abstract class Formule {
	
	/**
	 * Supprime les connecteurs 'implique' et 'equivalent' de la formule.
	 * Première étape de la mise sous forme normale.
	 * @return la formule sans les connecteurs 'equivalent' et 'implique' 
	 */
	public abstract Formule supprimeConnecteurs();
	
	/**
	 * Fait la negation.
	 * @return la negation de la formule
	 */
	public abstract Formule negation();
	
	/**
	 * Descend les operateurs 'Non' au niveau des atomes.
	 * Deuxième étape de la mise sous forme normale.
	 * @param isNegatif indique si la formule englobant la formule actuelle était une negation
	 * @return la formule avec les negations au niveau des atomes.
	 */
	public abstract Formule descendreNegation(boolean isNegatif);

	/**
	 * procedure de transport des quantifieurs en tête de formule.
	 * @return
	 */
	public Formule procedureTransportQ(){
		return TransporteurQuantifieurs.mettreQuantifieursDevant(this);
	}
	
	/**
	 * Fait remonter les quantifieurs d'un cran.
	 * @return
	 */
	public abstract Formule transportQuantificateurs();
	
	public Formule miseFormeSkolem(){
		return new Skolemisateur().miseEnForme(this);
	}
	
	public abstract Formule miseFormeClausale();
	
	/**
	 * Indique si les deux formules sont identique. (pas seulement equivalente)
	 * @param formule à comparer
	 * @return
	 */
	public abstract boolean isSame(Formule o);
	
	@Deprecated
	public abstract FormuleType getType();
	
	/**
	 * Renvois vrai si tous les quantifieurs sont devant.
	 * @param nonQuantifeur indique si la methode à rencontré une formule autre qu'un quantifieur
	 * @return
	 */
	public abstract boolean isQuantifieursFirsts(boolean nonQuantifeur);
	
	/**
	 * Renvois vrai si les quantifieurs existentiels sont avant les quantifieurs  universels.
	 * @param aUniversel indique si la methode à rencontré un quantifieur universel
	 * @return
	 */
	public abstract boolean isQuantifieursInOrder(boolean aUniversel);
	
}
